package TP;

public class Purse {
	final int MAX_BALANCE;
	int balance;
	byte[] pin;

    /*@ invariant 0 <= balance;
      @ invariant balance <= MAX_BALANCE;
      @ invariant pin != null;
      @ invariant pin.length == 4;
      @ invariant (\forall int i ; 0 <= i && i < pin.length ; 0 <= pin[i] && pin[i] <= 9);
      @*/
    
    /*@ normal_behavior
      @     requires amount >= 0;
      @     requires amount <= balance;
      @     assignable balance;
      @     ensures balance == \old(balance) - amount;
      @     ensures \result == balance;
      @ also
      @ exceptional_behavior
      @     requires amount > balance;
      @     assignable \nothing;
      @     signals (PurseException e)
      @         amount > balance &&
      @         balance == \old(balance);
      @*/
	int debit(int amount) throws PurseException {
		if (amount <= balance) {
			balance -= amount;
			return balance;
		} else {
			throw new PurseException("overdrawn by " + amount);
		}
	}

    /*@ normal_behavior
      @     requires amount >= 0;
      @     requires amount + balance <= MAX_BALANCE;
      @     assignable balance;
      @     ensures balance == \old(balance) + amount;
      @     ensures \result == balance;
      @ also
      @ exceptional_behavior
      @     requires amount + balance > MAX_BALANCE;
      @     assignable \nothing;
      @     signals (PurseException e)
      @         balance == \old(balance);
      @*/
	int deposit(int amount) throws PurseException {
		if (amount + balance > MAX_BALANCE) {
			throw new PurseException("max value excedeed by " + amount);
		} else {
			balance += amount;
			return balance;
		}
	}

    /*@ requires p != null;
      @ requires p.length >= 4;
      @ assignable \nothing;
      @ ensures \result == (\forall int i ; 0 <= i && i < 4 ; pin[i] == p[i]);
      @*/
	boolean checkPin(byte[] p) {
		boolean res = true;
		for (int i = 0; i < 4; i++) {
			res = res && pin[i] == p[i];
		}
		return res;
	}

    /*@ requires p != null;
      @ requires p.length >= 4;
      @ requires (\forall int i ; 0 <= i && i < 4 ; 0 <= p[i] && p[i] <= 9);
      @ requires mb >= 0;
      @ requires b >= 0;
      @ requires b <= mb;
      @ assignable MAX_BALANCE, balance, pin;
      @ ensures MAX_BALANCE == mb;
      @ ensures balance == b;
      @ ensures (\forall int i ; 0 <= i && i < 4 ; pin[i] == p[i]);
      @*/
	Purse(int mb, int b, byte[] p) {
		MAX_BALANCE = mb;
		balance = b;
		pin = new byte[4];
		for (int i = 0; i < 4; i++) {
			pin[i] = p[i];
		}
	}

}
